$\forall$$x$:Knd, $T$:Type. Normal($T$) $\Rightarrow$ Normal($x$ : $T$)